0 Prolog
↳1 PrologToPiTRSProof (⇒, 0 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 10 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 7 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 PiDP
↳24 PiDPToQDPProof (⇒, 0 ms)
↳25 QDP
↳26 MRRProof (⇔, 41 ms)
↳27 QDP
↳28 PisEmptyProof (⇔, 0 ms)
↳29 YES
conf_in_g(X) → U1_g(X, del2_in_ga(X, Z))
del2_in_ga(X, Y) → U4_ga(X, Y, del_in_aga(U, X, Z))
del_in_aga(X, .(X, T), T) → del_out_aga(X, .(X, T), T)
del_in_aga(X, .(H, T), .(H, T1)) → U6_aga(X, H, T, T1, del_in_aga(X, T, T1))
U6_aga(X, H, T, T1, del_out_aga(X, T, T1)) → del_out_aga(X, .(H, T), .(H, T1))
U4_ga(X, Y, del_out_aga(U, X, Z)) → U5_ga(X, Y, del_in_aga(V, Z, Y))
U5_ga(X, Y, del_out_aga(V, Z, Y)) → del2_out_ga(X, Y)
U1_g(X, del2_out_ga(X, Z)) → U2_g(X, del_in_aag(U, Y, Z))
del_in_aag(X, .(X, T), T) → del_out_aag(X, .(X, T), T)
del_in_aag(X, .(H, T), .(H, T1)) → U6_aag(X, H, T, T1, del_in_aag(X, T, T1))
U6_aag(X, H, T, T1, del_out_aag(X, T, T1)) → del_out_aag(X, .(H, T), .(H, T1))
U2_g(X, del_out_aag(U, Y, Z)) → U3_g(X, conf_in_g(Y))
U3_g(X, conf_out_g(Y)) → conf_out_g(X)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
conf_in_g(X) → U1_g(X, del2_in_ga(X, Z))
del2_in_ga(X, Y) → U4_ga(X, Y, del_in_aga(U, X, Z))
del_in_aga(X, .(X, T), T) → del_out_aga(X, .(X, T), T)
del_in_aga(X, .(H, T), .(H, T1)) → U6_aga(X, H, T, T1, del_in_aga(X, T, T1))
U6_aga(X, H, T, T1, del_out_aga(X, T, T1)) → del_out_aga(X, .(H, T), .(H, T1))
U4_ga(X, Y, del_out_aga(U, X, Z)) → U5_ga(X, Y, del_in_aga(V, Z, Y))
U5_ga(X, Y, del_out_aga(V, Z, Y)) → del2_out_ga(X, Y)
U1_g(X, del2_out_ga(X, Z)) → U2_g(X, del_in_aag(U, Y, Z))
del_in_aag(X, .(X, T), T) → del_out_aag(X, .(X, T), T)
del_in_aag(X, .(H, T), .(H, T1)) → U6_aag(X, H, T, T1, del_in_aag(X, T, T1))
U6_aag(X, H, T, T1, del_out_aag(X, T, T1)) → del_out_aag(X, .(H, T), .(H, T1))
U2_g(X, del_out_aag(U, Y, Z)) → U3_g(X, conf_in_g(Y))
U3_g(X, conf_out_g(Y)) → conf_out_g(X)
CONF_IN_G(X) → U1_G(X, del2_in_ga(X, Z))
CONF_IN_G(X) → DEL2_IN_GA(X, Z)
DEL2_IN_GA(X, Y) → U4_GA(X, Y, del_in_aga(U, X, Z))
DEL2_IN_GA(X, Y) → DEL_IN_AGA(U, X, Z)
DEL_IN_AGA(X, .(H, T), .(H, T1)) → U6_AGA(X, H, T, T1, del_in_aga(X, T, T1))
DEL_IN_AGA(X, .(H, T), .(H, T1)) → DEL_IN_AGA(X, T, T1)
U4_GA(X, Y, del_out_aga(U, X, Z)) → U5_GA(X, Y, del_in_aga(V, Z, Y))
U4_GA(X, Y, del_out_aga(U, X, Z)) → DEL_IN_AGA(V, Z, Y)
U1_G(X, del2_out_ga(X, Z)) → U2_G(X, del_in_aag(U, Y, Z))
U1_G(X, del2_out_ga(X, Z)) → DEL_IN_AAG(U, Y, Z)
DEL_IN_AAG(X, .(H, T), .(H, T1)) → U6_AAG(X, H, T, T1, del_in_aag(X, T, T1))
DEL_IN_AAG(X, .(H, T), .(H, T1)) → DEL_IN_AAG(X, T, T1)
U2_G(X, del_out_aag(U, Y, Z)) → U3_G(X, conf_in_g(Y))
U2_G(X, del_out_aag(U, Y, Z)) → CONF_IN_G(Y)
conf_in_g(X) → U1_g(X, del2_in_ga(X, Z))
del2_in_ga(X, Y) → U4_ga(X, Y, del_in_aga(U, X, Z))
del_in_aga(X, .(X, T), T) → del_out_aga(X, .(X, T), T)
del_in_aga(X, .(H, T), .(H, T1)) → U6_aga(X, H, T, T1, del_in_aga(X, T, T1))
U6_aga(X, H, T, T1, del_out_aga(X, T, T1)) → del_out_aga(X, .(H, T), .(H, T1))
U4_ga(X, Y, del_out_aga(U, X, Z)) → U5_ga(X, Y, del_in_aga(V, Z, Y))
U5_ga(X, Y, del_out_aga(V, Z, Y)) → del2_out_ga(X, Y)
U1_g(X, del2_out_ga(X, Z)) → U2_g(X, del_in_aag(U, Y, Z))
del_in_aag(X, .(X, T), T) → del_out_aag(X, .(X, T), T)
del_in_aag(X, .(H, T), .(H, T1)) → U6_aag(X, H, T, T1, del_in_aag(X, T, T1))
U6_aag(X, H, T, T1, del_out_aag(X, T, T1)) → del_out_aag(X, .(H, T), .(H, T1))
U2_g(X, del_out_aag(U, Y, Z)) → U3_g(X, conf_in_g(Y))
U3_g(X, conf_out_g(Y)) → conf_out_g(X)
CONF_IN_G(X) → U1_G(X, del2_in_ga(X, Z))
CONF_IN_G(X) → DEL2_IN_GA(X, Z)
DEL2_IN_GA(X, Y) → U4_GA(X, Y, del_in_aga(U, X, Z))
DEL2_IN_GA(X, Y) → DEL_IN_AGA(U, X, Z)
DEL_IN_AGA(X, .(H, T), .(H, T1)) → U6_AGA(X, H, T, T1, del_in_aga(X, T, T1))
DEL_IN_AGA(X, .(H, T), .(H, T1)) → DEL_IN_AGA(X, T, T1)
U4_GA(X, Y, del_out_aga(U, X, Z)) → U5_GA(X, Y, del_in_aga(V, Z, Y))
U4_GA(X, Y, del_out_aga(U, X, Z)) → DEL_IN_AGA(V, Z, Y)
U1_G(X, del2_out_ga(X, Z)) → U2_G(X, del_in_aag(U, Y, Z))
U1_G(X, del2_out_ga(X, Z)) → DEL_IN_AAG(U, Y, Z)
DEL_IN_AAG(X, .(H, T), .(H, T1)) → U6_AAG(X, H, T, T1, del_in_aag(X, T, T1))
DEL_IN_AAG(X, .(H, T), .(H, T1)) → DEL_IN_AAG(X, T, T1)
U2_G(X, del_out_aag(U, Y, Z)) → U3_G(X, conf_in_g(Y))
U2_G(X, del_out_aag(U, Y, Z)) → CONF_IN_G(Y)
conf_in_g(X) → U1_g(X, del2_in_ga(X, Z))
del2_in_ga(X, Y) → U4_ga(X, Y, del_in_aga(U, X, Z))
del_in_aga(X, .(X, T), T) → del_out_aga(X, .(X, T), T)
del_in_aga(X, .(H, T), .(H, T1)) → U6_aga(X, H, T, T1, del_in_aga(X, T, T1))
U6_aga(X, H, T, T1, del_out_aga(X, T, T1)) → del_out_aga(X, .(H, T), .(H, T1))
U4_ga(X, Y, del_out_aga(U, X, Z)) → U5_ga(X, Y, del_in_aga(V, Z, Y))
U5_ga(X, Y, del_out_aga(V, Z, Y)) → del2_out_ga(X, Y)
U1_g(X, del2_out_ga(X, Z)) → U2_g(X, del_in_aag(U, Y, Z))
del_in_aag(X, .(X, T), T) → del_out_aag(X, .(X, T), T)
del_in_aag(X, .(H, T), .(H, T1)) → U6_aag(X, H, T, T1, del_in_aag(X, T, T1))
U6_aag(X, H, T, T1, del_out_aag(X, T, T1)) → del_out_aag(X, .(H, T), .(H, T1))
U2_g(X, del_out_aag(U, Y, Z)) → U3_g(X, conf_in_g(Y))
U3_g(X, conf_out_g(Y)) → conf_out_g(X)
DEL_IN_AAG(X, .(H, T), .(H, T1)) → DEL_IN_AAG(X, T, T1)
conf_in_g(X) → U1_g(X, del2_in_ga(X, Z))
del2_in_ga(X, Y) → U4_ga(X, Y, del_in_aga(U, X, Z))
del_in_aga(X, .(X, T), T) → del_out_aga(X, .(X, T), T)
del_in_aga(X, .(H, T), .(H, T1)) → U6_aga(X, H, T, T1, del_in_aga(X, T, T1))
U6_aga(X, H, T, T1, del_out_aga(X, T, T1)) → del_out_aga(X, .(H, T), .(H, T1))
U4_ga(X, Y, del_out_aga(U, X, Z)) → U5_ga(X, Y, del_in_aga(V, Z, Y))
U5_ga(X, Y, del_out_aga(V, Z, Y)) → del2_out_ga(X, Y)
U1_g(X, del2_out_ga(X, Z)) → U2_g(X, del_in_aag(U, Y, Z))
del_in_aag(X, .(X, T), T) → del_out_aag(X, .(X, T), T)
del_in_aag(X, .(H, T), .(H, T1)) → U6_aag(X, H, T, T1, del_in_aag(X, T, T1))
U6_aag(X, H, T, T1, del_out_aag(X, T, T1)) → del_out_aag(X, .(H, T), .(H, T1))
U2_g(X, del_out_aag(U, Y, Z)) → U3_g(X, conf_in_g(Y))
U3_g(X, conf_out_g(Y)) → conf_out_g(X)
DEL_IN_AAG(X, .(H, T), .(H, T1)) → DEL_IN_AAG(X, T, T1)
DEL_IN_AAG(.(T1)) → DEL_IN_AAG(T1)
From the DPs we obtained the following set of size-change graphs:
DEL_IN_AGA(X, .(H, T), .(H, T1)) → DEL_IN_AGA(X, T, T1)
conf_in_g(X) → U1_g(X, del2_in_ga(X, Z))
del2_in_ga(X, Y) → U4_ga(X, Y, del_in_aga(U, X, Z))
del_in_aga(X, .(X, T), T) → del_out_aga(X, .(X, T), T)
del_in_aga(X, .(H, T), .(H, T1)) → U6_aga(X, H, T, T1, del_in_aga(X, T, T1))
U6_aga(X, H, T, T1, del_out_aga(X, T, T1)) → del_out_aga(X, .(H, T), .(H, T1))
U4_ga(X, Y, del_out_aga(U, X, Z)) → U5_ga(X, Y, del_in_aga(V, Z, Y))
U5_ga(X, Y, del_out_aga(V, Z, Y)) → del2_out_ga(X, Y)
U1_g(X, del2_out_ga(X, Z)) → U2_g(X, del_in_aag(U, Y, Z))
del_in_aag(X, .(X, T), T) → del_out_aag(X, .(X, T), T)
del_in_aag(X, .(H, T), .(H, T1)) → U6_aag(X, H, T, T1, del_in_aag(X, T, T1))
U6_aag(X, H, T, T1, del_out_aag(X, T, T1)) → del_out_aag(X, .(H, T), .(H, T1))
U2_g(X, del_out_aag(U, Y, Z)) → U3_g(X, conf_in_g(Y))
U3_g(X, conf_out_g(Y)) → conf_out_g(X)
DEL_IN_AGA(X, .(H, T), .(H, T1)) → DEL_IN_AGA(X, T, T1)
DEL_IN_AGA(.(T)) → DEL_IN_AGA(T)
From the DPs we obtained the following set of size-change graphs:
U1_G(X, del2_out_ga(X, Z)) → U2_G(X, del_in_aag(U, Y, Z))
U2_G(X, del_out_aag(U, Y, Z)) → CONF_IN_G(Y)
CONF_IN_G(X) → U1_G(X, del2_in_ga(X, Z))
conf_in_g(X) → U1_g(X, del2_in_ga(X, Z))
del2_in_ga(X, Y) → U4_ga(X, Y, del_in_aga(U, X, Z))
del_in_aga(X, .(X, T), T) → del_out_aga(X, .(X, T), T)
del_in_aga(X, .(H, T), .(H, T1)) → U6_aga(X, H, T, T1, del_in_aga(X, T, T1))
U6_aga(X, H, T, T1, del_out_aga(X, T, T1)) → del_out_aga(X, .(H, T), .(H, T1))
U4_ga(X, Y, del_out_aga(U, X, Z)) → U5_ga(X, Y, del_in_aga(V, Z, Y))
U5_ga(X, Y, del_out_aga(V, Z, Y)) → del2_out_ga(X, Y)
U1_g(X, del2_out_ga(X, Z)) → U2_g(X, del_in_aag(U, Y, Z))
del_in_aag(X, .(X, T), T) → del_out_aag(X, .(X, T), T)
del_in_aag(X, .(H, T), .(H, T1)) → U6_aag(X, H, T, T1, del_in_aag(X, T, T1))
U6_aag(X, H, T, T1, del_out_aag(X, T, T1)) → del_out_aag(X, .(H, T), .(H, T1))
U2_g(X, del_out_aag(U, Y, Z)) → U3_g(X, conf_in_g(Y))
U3_g(X, conf_out_g(Y)) → conf_out_g(X)
U1_G(X, del2_out_ga(X, Z)) → U2_G(X, del_in_aag(U, Y, Z))
U2_G(X, del_out_aag(U, Y, Z)) → CONF_IN_G(Y)
CONF_IN_G(X) → U1_G(X, del2_in_ga(X, Z))
del_in_aag(X, .(X, T), T) → del_out_aag(X, .(X, T), T)
del_in_aag(X, .(H, T), .(H, T1)) → U6_aag(X, H, T, T1, del_in_aag(X, T, T1))
del2_in_ga(X, Y) → U4_ga(X, Y, del_in_aga(U, X, Z))
U6_aag(X, H, T, T1, del_out_aag(X, T, T1)) → del_out_aag(X, .(H, T), .(H, T1))
U4_ga(X, Y, del_out_aga(U, X, Z)) → U5_ga(X, Y, del_in_aga(V, Z, Y))
del_in_aga(X, .(X, T), T) → del_out_aga(X, .(X, T), T)
del_in_aga(X, .(H, T), .(H, T1)) → U6_aga(X, H, T, T1, del_in_aga(X, T, T1))
U5_ga(X, Y, del_out_aga(V, Z, Y)) → del2_out_ga(X, Y)
U6_aga(X, H, T, T1, del_out_aga(X, T, T1)) → del_out_aga(X, .(H, T), .(H, T1))
U1_G(del2_out_ga(Z)) → U2_G(del_in_aag(Z))
U2_G(del_out_aag(Y)) → CONF_IN_G(Y)
CONF_IN_G(X) → U1_G(del2_in_ga(X))
del_in_aag(T) → del_out_aag(.(T))
del_in_aag(.(T1)) → U6_aag(del_in_aag(T1))
del2_in_ga(X) → U4_ga(del_in_aga(X))
U6_aag(del_out_aag(T)) → del_out_aag(.(T))
U4_ga(del_out_aga(Z)) → U5_ga(del_in_aga(Z))
del_in_aga(.(T)) → del_out_aga(T)
del_in_aga(.(T)) → U6_aga(del_in_aga(T))
U5_ga(del_out_aga(Y)) → del2_out_ga(Y)
U6_aga(del_out_aga(T1)) → del_out_aga(.(T1))
del_in_aag(x0)
del2_in_ga(x0)
U6_aag(x0)
U4_ga(x0)
del_in_aga(x0)
U5_ga(x0)
U6_aga(x0)
U1_G(del2_out_ga(Z)) → U2_G(del_in_aag(Z))
U2_G(del_out_aag(Y)) → CONF_IN_G(Y)
CONF_IN_G(X) → U1_G(del2_in_ga(X))
del_in_aag(T) → del_out_aag(.(T))
del_in_aag(.(T1)) → U6_aag(del_in_aag(T1))
del2_in_ga(X) → U4_ga(del_in_aga(X))
U6_aag(del_out_aag(T)) → del_out_aag(.(T))
U4_ga(del_out_aga(Z)) → U5_ga(del_in_aga(Z))
del_in_aga(.(T)) → del_out_aga(T)
del_in_aga(.(T)) → U6_aga(del_in_aga(T))
U5_ga(del_out_aga(Y)) → del2_out_ga(Y)
U6_aga(del_out_aga(T1)) → del_out_aga(.(T1))
del2inga1 > U4ga1 > U1G1 > U2G1 > CONFING1 > delinaag1 > delinaga1 > U6aga1 > del2outga1 > U5ga1 > deloutaga1 > U6aag1 > deloutaag1 > .1
del_in_aag_1=3
del_out_aag_1=1
._1=2
U6_aag_1=2
del2_in_ga_1=4
U4_ga_1=1
del_in_aga_1=3
del_out_aga_1=5
U5_ga_1=3
U6_aga_1=2
del2_out_ga_1=7
U1_G_1=1
U2_G_1=5
CONF_IN_G_1=6
del_in_aag(x0)
del2_in_ga(x0)
U6_aag(x0)
U4_ga(x0)
del_in_aga(x0)
U5_ga(x0)
U6_aga(x0)